3.4 例題 | オブジェクト移送 |
3.4.3 本実装の場合
問題を以下に示すように簡略化し，その条件のもとで例題の実行を試みる．図3.12では，
ノードは2個，移送先は必ず移送させたいオブジェクトが属するノードと異なるものが指 定されるようになっている．つまり必ずオブジェクトの移送が確実に実行されることにな る．また，実行手順は図3.11中のコメントに従っている．図3.11のプログラムでは各手順 とも Migrator オブジェクトの属するグループ(ノード)のEvaluator オブジェクトによっ てメタレベル実行されている．本実装では，メタレベル実行されたという仮定のもとに必 要と思われる関数を定義し，例題を実行した．
--移送先が別のグループ
rewrite (MCON ((MIGRATE oid target des):msgs)
((MI oid' localdb nodeset):objs))
| oid == oid' && mig /= []
-- 移送元の Database オブジェクトからオブジェクトを削除する
= rewrite (MCON ((DBDEL localdb target):msgs)
((MI oid' localdb nodeset):objs))
where (mig,(MCON ms os))
-- 移送先の Migrator オブジェクトのアドレスを獲得する
= find_migrator des nodeset
where
find_migrator des nodeset
| [des] == nodeset
= ([],MCON [] [])
| des == "mh1"
= (find_migrator_sub conf2, conf2)
| des == "mh2"
= (find_migrator_sub conf1, conf1)
where find_migrator_sub (MCON m ((MI oid _ _):_))
= oid
find_migrator_sub (MCON m (_:r))
= find_migrator_sub (MCON m r)
-- 移送先の Datbase オブジェクトのアドレスを獲得する
db = find_destination_db os
where find_destination_db ((DB db _ _):_)
= db
find_destination_db (_:rest)
= find_destination_db rest
-- 移送を実行する
result = rewrite (MCON ((DBADD db target):ms) os)
図3.12: オブジェクト移送に関する書き換え規則
---- 例題用のデータ定義
---- ノード N1 内のオブジェクト
mh1 = MH "mh1" "th1" []
th1 = TH "th1" "mh1" "db1" "ev1" 1
db1 = DB "db1" acceptable1 objlist1
ev1 = EV "ev1" "mh1" "db1" 1
mi1 = MI "mi1" "db1" ["N2"]
conf11 = MCON [msg11] [mi1,mh1, th1, db1, ev1]
conf12 = MCON [msg12] [mi1,mh1, th1, db1, ev1]
msg11 = MIGRATE "mi1" oa1 "mh2"
msg12 = MIGRATE "mi1" oa1 "mh1"
acceptable1 = [("A1","mem"),("A1","add"),("A1","del"),
("B1","mem"),("B1","add"),("B1","del"),
("C1","mem"),("C1","add"),("C1","del")]
objlist1 = [("A1",oa1),("B1",ob1),("C1",oc1)]
-- ノード N2 内のオブジェクト
mh2 = MH "mh2" "th2" []
th2 = TH "th2" "mh2" "db2" "ev2" 1
db2 = DB "db2" acceptable2 objlist2
ev2 = EV "ev2" "mh2" "db2" 1
mi2 = MI "mi2" "db" ["mh1"]
conf2 = MCON [] [mh2, th2, db2, ev2, mi2]
acceptable2 = [("A2","mem"),("A2","add"),("A2","del"),
("B2","mem"),("B2","add"),("B2","del"),
("C2","mem"),("C2","add"),("C2","del")]
objlist2 = [("A2",oa2),("B2",ob2),("C2",oc2)]
-- ノード N1,N2 のベースレベルのオブジェクトの定義
oa1 = OBJ "A1" [("member",["a11","a12","a13"])]
ob1 = OBJ "B1" [("member",["b11","b12","b13"])]
oc1 = OBJ "C1" [("member",["c11","c12","c13"])]
oa2 = OBJ "A2" [("member",["a21","a22","a23"])]
ob2 = OBJ "B2" [("member",["b21","b22","b23"])]
oc2 = OBJ "C2" [("member",["c21","c22","c23"])]
図3.13: 例題のデータ
-- 例題の実行
-- ノード N1 のオブジェクト A1 を ノード N2 へ移送する
-- 実行前のノード N1
N1 = MCON [] [MH "mh1" "th1" [],
TH "th1" "mh1" "db1""ev1" 1,
DB "db1" [("A1","mem"), ("A1","add"), ("A1","del")，
("B1","mem"), ("B1","add"), ("B1","del"),
[("A1",OBJ "A1" [("member",["a11","a12","a13"])]),
("B1",OBJ "B1" [("member",["b11","b12","b13"])]),
("C1",OBJ "C1" [("member",["c11","c12","c13"])])],
EV "ev1" "mh1" "db1" 1,
MI "mi1" "db1" ["N2"]]
-- 実行前のノード N2
N2 = MCON [] [MH "mh2" "th2" [],
TH "th2" "mh2" "db2" "ev2" 1,
DB "db2" [("A2","mem"), ("A2","add"), ("A2","del"),
("B2","mem"), ("B2","add"), ("B2","del"),
("C2","mem"), ("C2","add"), ("C2","del")]
[("A2",OBJ "A2" [("member",["a21","a22","a23"])]),
("B2",OBJ "B2" [("member",["b21","b22","b23"])]),
("C2",OBJ "C2" [("member",["c21","c22","c23"])])]
EV "ev2" "mh2" "db2" 1,
MI "mi2" "db2" ["N1"]]
---実行後のノードN1
N1 = MCON [] [DB "db1" [("B1","mem"), ("B1","add"), ("B1","del"),
("C1","mem"), ("C1","add"), ("C1","del")]
[("B1",OBJ "B1" [("member",["b11","b12","b13"])]),
("C1",OBJ "C1" [("member",["c11","c12","c13"])])],
EV "ev1" "mh1" "db1" 1,
MI "mi1" "db1" ["N2"],
MH "mh1" "th1" [],
TH "th1" "mh1" "db1""ev1" 1]
---実行後のノードN2
N2 = MCON [] [DB "db2" [("A2","mem"), ("A2","add"), ("A2","del"),
("B2","mem"), ("B2","add"), ("B2","del"),
("C2","mem"), ("C2","add"), ("C2","del"),
("A1","mem"), ("A1","add"), ("A1","del")]
[("A2",OBJ "A2" [("member",["a21","a22","a23"])]),
("B2",OBJ "B2" [("member",["b21","b22","b23"])]),
("C2",OBJ "C2" [("member",["c21","c22","c23"])]),
("A1",OBJ "A1" [("member",["a11","a12","a13"])])],
EV "ev2" "mh2" "db2" 1,
MI "mi2" "db2" ["N1"],
MH "mh2" "th2" [],
TH "th2" "mh2" "db2" "ev2" 1]
図3.14: 例題の実行例
詳細な実行手順は省略したが，図3.14中の実行前後の各ノードのデータベースの中身を 比較すると，ノード N1のオブジェクトOBJ "A1" ["member",["a11","a12","a13"]]が ノード N2のデータベースに移動していることがわかる．
3.4.4
メタレベルシステムの正当性
書き換え論理に基づいた宣言的記述を利用してそのシステムの様々な性質を解析するこ とが可能と予測される．本研究ではそのうちの一つと考えられる，メタレベルシステムの 正当性の証明を行った．
ここで，メタレベルシステムが正当であるとは，
ベースレベルシステムの一回の遷移(書き換え)に対し，それをシミュレートするよ うなメタレベルシステムの(複数回の)遷移が存在し，
ベースレベルシステムのメタレベル表現が変化するようなメタレベルシステムでの遷 移に対し，それに対応するベースレベルシステムでの一回の遷移が存在する
ことを意味する[45]．本研究では，オブジェクト移送の例題の記述を基礎とし，メタコン フィギュレーションに関する構造帰納法[49]を用いて，メタレベルシステムが上記の意味 で正当であることを証明した．具体的には以下のように証明している．
記法の定義
以下のように記法の定義を行う．
記法 その意味
S 項からなる(ベースレベル)システム
C S のコンフィギュレーションで，hM;Oi と書く
M C のメッセージの集合
O C のオブジェクトの集合
R S の書き換え規則の集合
0
S
S のすべてのコンフィギュレーションの集合
0
"S
S のメタレベル表現"S に関するすべてのコンフィギュレーション
(メタコンフィギュレーションとよぶ)の集合
R "S の書き換え規則の集合
hnjattsi 名前 n，属性atts をもつオブジェクト
[t;v] ターゲットt に値 v を送信するメッセージ
(t1!t2) 以下に示す書き換え規則の略記
[t1;v] ht1jattsi ! [t2;v] ht1jattsi
または
[t1;v] ht1jattsi ! [t2;v] ht1jattsiht3jatts 0
i
"C C のメタレベル表現(メタコンフィギュレーション)
"M "C のメッセージの集合
O (O;R ) "C のオブジェクトの集合
この集合に属しているデータベースオブジェクトは
O とR のメタレベル表現をデータとして持っている
表3.2: 記法の定義
表中において，S をシステム，"S をシステムS のメタレベル表現とする．ここで，シス テムS は各々項で定義されたオブジェクトのグループ，メッセージ，および書き換え規則 から構成されているものとする．
本研究においては，"S は5種類の特徴づけられたオブジェクトから構成されている．そ れらは各々メッセージハンドラ(MessageHandler, mh と略記，以下同様),タスクハンドラ
(Task Handler,th)，データベース(Databasedb)，エバリュエータ(Evaluator,ev)，およ びth に対応するカスタマ (Customer, cus) である．文献[45] で定義されているこれらの オブジェクトは本研究でもほぼ同様な役割を果たしている．詳細は以下の通りである．
メッセージハンドラ(Message Handler, mh):
メッセージハンドラは"S もしくは "S 以外のシステムからのメッセージを受理し，
その送信先を確認して "S 内のタスクハンド ラもしくは "S 以外のメッセージハン ドラに再送信する．
タスクハンドラ (TaskHandler, th):
タスクハンド ラは自分自身が属しているシステムのすべての(メタレベル)オブジェ クトを把握している．このオブジェクトはベースレベルで処理されるメッセージのメ タレベル表現に関して，メタレベル計算の準備を行う．タスクハンドラがメッセージ ハンドラによって送信されたメタメッセージを受理すると，続いて実行すべき計算を 続けるためのオブジェクト(後述)を生成する．
データベース(Database, db):
データベースは S のオブジェクトおよび書き換え規則のメタレベル表現をデータと して保持している．
エバリュエータ(Evaluator,ev):
エバリュエータはメッセージ，オブジェクト，書き換え規則のメタレベル表現を受け 取り，規則で規定された遷移を実行する．
m をS 内のあるメッセージを表現するものと仮定する．そのとき，m のメタレベル表 現は"m と表現する．さらに，"m に対応するメタメッセージは[mh;"m] と表現する．S のすべての書き換え規則は"S を構成するオブジェクトdb のデータとしてメタレベル表現 される．
表3.2 の記法を用いて，コンフィギュレーションC のメッセージの集合 M のメタレベ ル表現，メタコンフィギュレーション"C，および"S の書き換え規則の集合R を以下の ように定義する．
"M = f[mh;"m] jm2Mg
"C = h"M;O(O;R)i
R = f(mh !th);(mh!omh);(th! db);(db!cus);
(cus!ev);(cus!mh);(ev!db)g
ここで，omhは "S 以外のメッセージハンドラの名前である．
さらに，遷移関係とコンフィギュレーション間の遷移列は表3.3 にあるように定義される．
記法 その意味
C
1
0!C
2 0
S に属する C1 にR のある書き換え規則を1回適用した結果
0
S に属する C2 に遷移する．
もしC1 に適用した書き換え規則r を明示したい場合は
C
1 r
0!C
2 と表現する．
K
1 (n)
0!K
2 0
"S に属するK1 にR の適当な書き換え規則をn 回適用すると
0
"S に属するK2 に遷移する．
ただし，この書き換えによってS のオブジェクトや書き換え 規則のメタレベル表現は変化していないものとする．
表3.3: 遷移関係の定義 証明の概要
証明を始める前に次のことに注意しておく．それは，
0
"S に属する任意のメタコンフィギュレーションK に対し，それに対応する0S
に属するコンフィギュレーション C が必ず存在する
ということ，すなわち，K は C のメタレベル表現のひとつであるということである．そ こで表3.3 で与えた遷移列の定義を利用し集合
"C =fK 20
"S
jK 0!"C ; or "C 0!Kg
を定義する．ここで，K が0"S の要素であるとき，遷移列の定義から，"C の要素ならば
S におけるオブジェクトと書き換え規則のメタレベル表現は"C と一致していることに注 意する．また，0
↑
S= ()
! における擬似遷移関係
=)を以下のように定義する．
定義: もし，"C1の任意の元K1に対して
K
1 (3)
0!
0! (3)
0!K
2
を満たす"C2の要素K2が存在するとき，"C1と"C2は擬似遷移関係にあるといい，
"C
1
=)"C
2と書く．ただし，0(3)! はデータベースの内容を書き換えない任意回数の書き 換え列，0!はデータベースの内容を書き換えるRの書き換え規則 の適用を意味する．
以上の準備によって，"S が正当であるということは次の定理にまとめることができる．
定理: C1;C2 は0S の要素であると仮定する．このとき，"C1
=)"C
2 であることの必 要十分条件はC1 0!r C2 を満たすR の書き換え規則r が存在することである．ここで，
=) は0"S
= ()
! における擬似遷移関係である．
この定理の証明の概要は次のようになる．
必要性: 必要性を示すためには "C1 03! "C2 が成り立つことを確認すれば良い．m を ベースレベルの書き換え規則r を1回適用してC1 をC2 に遷移させるベースレベルのメッ セージであるとする．このとき，mのメタレベル表現は[mh;"m] という形のメッセージが 持っている値として出現する．この値"m に留意し以下のような実際に生じる遷移列を生 成することが可能である．0!
n
は以下の遷移列におけるn 回目の書き換えであることを示 している．
"C
1
=h"M
1
;O(O
1
;R )i
=hf[mh;"m]g ["M 0
1
;O(O
1
;R )i 0!
1
hf[th;"m]g ["M 0
1
;O (O
1
;R)i
0!
2
hf[db;"m]g ["M 0
1
;O (O
1
;R)[fcus("m)gi
0!
3
hf[cus;"m]g ["M 0
1
;O(O
1
;R)[fcus("m)gi
0!
4
hf[ev;"m]g ["M 0
1
;O (O
1
;R)i
0!
5
h"M 0
1
["M
1 00
;O(mod(O
1 );R)i
= h"M
2
;O(O
2
;R)i = "C
2
ここで，M0
1
=M
1
0fmg である．さらに，M1
00 は書き換え規則r の右辺に出現するメッ セージの集合を，mod(O1
) は書き換え規則r によってO1 を変更したオブジェクトもしく は，新たに生成されたオブジェクトの集合を表現している．
各々の書き換えステップの説明は以下の通りである．
1: "C の書き換え規則 (mh ! th) は mh が[mh;"m] という形をした "C1 のメタメッ セージを受理した場合に適用される．
2: 書き換え規則(th!db) はthがメタメッセージ[th;"m]を受理した場合に適用され る．このとき，新たなオブジェクト(タスクハンドラのカスタマ(customer))cus("m)
がその規則によって生成される．
3: 書き換え規則(db!cus) はdb がメタメッセージ[db;"m] を受理した場合に適用さ れる．
4: 書き換え規則(cus! ev) はcus("m) がメタメッセージ [cus;"m] を受理した場合 に適用される．このとき，2 で生成されたオブジェクト cus("m) はこの書き換え規 則を適用することによって消去される．
5: 書き換え規則 (ev !db) はdb がメタメッセージ[ev;"m] を受理した場合に適用さ れる．このとき，この書き換え規則によって，メッセージm に関するメタレベル実 行が引き起こされる．
5 番目の書き換えステップではメタレベル実行が引き起こされる．それは書き換え規則
(ev !db) はベースレベルのオブジェクトおよび書き換え規則のメタレベル表現を変更す ることを意味している．さらに，その書き換え規則によって幾つかの新たなメッセージが 送信されている可能性がある．それらのメッセージの各々は書き換え規則r によって送信 されたメッセージのメタレベル表現を値として保持している．
このようにして"M10
["M 00
1
=M
2 かつmod(O1)=O2 を得ることができた．よって必 要性は証明された．
十分性: 十分性を示すために，まず次の補題を証明しておく．
補題: 0"S の要素である任意のK に対して，K 0(n)!K0 かつ
M(K 0
)=f[ev;"m]j m2Mgが成立するような0"S の要素であるK0 と自然数n が存在